(set-logic QF_BV)
(set-option :opt.priority box)
(set-option :opt.maxsat_engine maxres)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const bv_12-0 (_ BitVec 12))
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const bv_4-0 (_ BitVec 4))
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const bv_21-4 (_ BitVec 21))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v5 (= #b110010111 #b110010111 #b110010111)))
(assert (or v4 (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v5))
(assert (or v5 v3 (bvuge #b110010111 #b110010111)))
(assert (or (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v2))
(assert (or (bvsle #b110010111 #b110010111) v2 (bvsle #b110010111 #b110010111)))
(assert (or v2 (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) v6))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v5 v3))
(assert (or v4 (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111))))
(assert (or (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v6))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v3 (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111))))
(assert (or v4 (bvsle #b110010111 #b110010111) v6))
(assert (or v2 v0 (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0)))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvsle #b110010111 #b110010111) v2))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v0 v5))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v3 v3))
(assert (or (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) v2 v5))
(assert (or v5 (bvsle #b110010111 #b110010111) v2))
(assert (or (= #b110010111 #b110010111 #b110010111) v2 v2))
(assert (or (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) (bvsle #b110010111 #b110010111) v0))
(assert (or v3 (= #b110010111 #b110010111 #b110010111) (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111))))
(assert (or (= #b110010111 #b110010111 #b110010111) (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0))))
(assert (or v0 (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0)))
(assert (or v6 (= #b110010111 #b110010111 #b110010111) (= #b110010111 #b110010111 #b110010111)))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v3 (bvsle #b110010111 #b110010111)))
(assert (or v3 (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v6))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v2 (= #b110010111 #b110010111 #b110010111)))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111) (= #b110010111 #b110010111 #b110010111)))
(assert (or v0 v2 v0))
(assert (or v2 (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (bvsle #b110010111 #b110010111)))
(assert (or v3 v2 v6))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0))))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (= #b110010111 #b110010111 #b110010111) (bvsle #b110010111 #b110010111)))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) (= #b110010111 #b110010111 #b110010111)))
(assert (or v6 (distinct (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (distinct #b110010111 #b110010111 #b110010111) (and (= bv_12-0 bv_12-0 bv_12-0) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (or (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) (bvsle #b110010111 #b110010111)) (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0) (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v1) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) (not v2) (xor (distinct #b110010111 #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0) v3 (distinct #b110010111 #b110010111 #b110010111) (=> v2 (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0)) v2 (= bv_12-0 bv_12-0 bv_12-0)) (bvuge #b110010111 #b110010111)) (bvuge #b110010111 #b110010111)))
(assert (or v6 (bvuge #b110010111 #b110010111) (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0))))
(assert (or (bvuge (bvneg (bvashr (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) (bvor (concat #b110010111 bv_12-0) (concat #b110010111 bv_12-0))) v5 v5))
(assert (or (= (distinct bv_12-0 bv_12-0 bv_12-0 bv_12-0) v0 (bvsle #b110010111 #b110010111) (= bv_12-0 bv_12-0 bv_12-0)) v3 (= bv_12-0 (bvsmod bv_12-0 bv_12-0) bv_12-0)))
(assert (or v3 v3 (bvsle #b110010111 #b110010111)))
(assert (or v6 v5 (bvuge #b110010111 #b110010111)))
(minimize bv_12-0)
(minimize bv_21-4)
(check-sat)
(exit)
